﻿module AbstractDomain

type abstractValue = AbstractValue of int with
    static member inline op_Equality (AbstractValue(x), AbstractValue(y)) = x=y

let none = AbstractValue 0
let copy  = AbstractValue 10
let additive = AbstractValue 15
let linearPolynomial = AbstractValue 20
let polynomial  = AbstractValue 30
let exponentialAtLeast = AbstractValue 40
let lub (AbstractValue x) (AbstractValue y) = AbstractValue(max x y)

let sum a b =
    if (a=exponentialAtLeast) || (b=exponentialAtLeast) then exponentialAtLeast
    elif (a=none) then b
    elif (b=none) then a
    else polynomial

let prod(((AbstractValue x) as a), ((AbstractValue y) as b)) =
    if ((a=none) || (b = none)) then none else AbstractValue(max x y)

let isLinear v = (v = copy || v = additive)

let toString v =
    match v with
      | AbstractValue 0 -> "0"
      | AbstractValue 10 -> "1"
      | AbstractValue 15 -> "1+"
      | AbstractValue 20 -> "2"
      | AbstractValue 30 -> "3"
      | AbstractValue 40 -> "4"
      | _ -> "Unknown value"